es-real{i:l}
es-real(es.locl(mkid{b:ut2}) sends [mkid{tg:ut2},x.x{}(mkid{done:ut2})] on link mklnk{loc1:ut2,
es-real(es.locl(mkid{b:ut2}) sends [mkid{tg:ut2},x.x{}(mkid{done:ut2})] on link mklnk{loc2:ut2,
es-real(es.locl(mkid{b:ut2}) sends [mkid{tg:ut2},x.x{}(mkid{done:ut2})] on link mklnk{1:ut2
es-real(es.locl(mkid{b:ut2}) sends [mkid{tg:ut2},x.x{}(mkid{done:ut2})] on link mklnk{} once
es-real() 

latex

Definitions	A c B, P  Q, Id, t  T, normal-type{i:l}(T), IdLnk, mklnk{$a:ut2, $b:ut2, $n:ut2}, mkid{$x:ut2}, P  Q, x:A. B(x)
Lemmas	bool-inhabited, bool wf, send-once-realizable